We study the termination of rewriting modulo a set of equations in theCalculus of Algebraic Constructions, an extension of the Calculus ofConstructions with functions and predicates defined by higher-order rewriterules. In a previous work, we defined general syntactic conditions based on thenotion of computable closure for ensuring the termination of the combination ofrewriting and beta-reduction. Here, we show that this result is preserved whenconsidering rewriting modulo a set of equations if the equivalence classesgenerated by these equations are finite, the equations are linear and satisfygeneral syntactic conditions also based on the notion of computable closure.This includes equations like associativity and commutativity, and provides anoriginal treatment of termination modulo equations.
展开▼
